perm filename PROVER.DOC[1,JRA]2 blob
sn#034727 filedate 1973-04-12 generic text, type T, neo UTF8
PRELIMINARY USER'S MANUAL
FOR
INTERACTIVE THEOREM PROVER
BY
JOHN ALLEN
Preface
This document represents a short guide to using a development of the
program originally described in Allen and Luckham [MI5]. Many of the
later sections ,on pattern matching and subroutining especially, are
still in a rudimentary stage of development. Experiments
demonstrating various applications of the strategies and the user
oriented features are described in a forthcoming report,
"Applications of First Order Proof Procedures" by Allen, Luckham, and
Morales.
Preliminary User's Manual April 12, 1973
Preliminary User's Manual for the Theorem Prover
The current program is a resolution- and paramodulation-based theorem
prover with extensive facilities for on-line control. Many of the
other facilities are quite rudimentary. The pattern matching and
subroutining aspects of the prover will be revised significantly.
Perhaps the easiest introduction is to follow the development of a
few examples.
Example 1.
Consider the following simple problem from propositional calculus:
Given A ⊃ B, and ¬A ⊃ B, prove B.
This problem could be presented to the prover as:
PRE_PRED: A,B;
HYPS: A⊃B;
¬A⊃B;
THM: B;
;
Or perhaps in a less trivial vein:
Example 2.
Consider the following set of statements:
(1) (∀x∀y){P(x,y) ∧ P(y z) ⊃ G(x,z)}
(2) (∀y∃x){P(x,y)}
We might interpret these statements as claiming
"For all x and y, if x is the parent of y and y is the parent
of z, then x is the grandparent of z,"
and
"Everyone has a parent."
Given these statements as hypotheses we might wish to know if there
were individuals, x and y such that x is the grandparent of y. We
could pose that question as the statement:
1
Preliminary User's Manual April 12, 1973
(3) (∃x∃y){G(x,y)}
It is clear that (3) does indeed follow from (1) and (2). How do we
formulate the problem for the theorem prover?
Here is one axiomatization:
PRE_PRED: P,G;
VAR:x,y,z;
G1: ∀(x,y)(P(x,y) ∧ P(y,z) ⊃ G(x,z));
G2: ∀y∃x P(x,y);
THM: ∃(x,y)G(x,y);
;
Some of the conventions displayed in the examples are:
(1) the predicate letters and function symbols must be declared
according to their type. For example infix and prefix operators are
declared by INF_OP and PRE_OP respectively. Constants are considered
to be prefix operators of zero arguments. Similarly infix and prefix
predicate symbols must be declared as INF_PRED and PRE_PRED
respectively. Propositional letters should be declared to be prefix
predicate symbols. (2) variables must be declared;actually the
effect of the variable declaration is to declare the identifier as a
variable prefix. The set of variables is automatically augmented to
include 9 additional `subscripted' variants of each declared
variable. For example,if x any y are declared variables then
x1,x2,..,x9,y1,y2...,y9 . are also variables and need not be
declared. (3) each statement must be terminated with a semi-colon;
(4) statements or sets of statements may be labeled. These labels
2
Preliminary User's Manual April 12, 1973
can by used to refer to clauses in the on-line editor. If a
statement is labeled, THM, then the negation of that statement is
formed and is used in the list of input statements. The identifier
used to name the theorem may be changed by modifying the LISP value
of the atom THEOREMNAME.(Thus the default value of THEOREMNAME is
THM.) (5) adjacent like quantifiers may combined. (6) the whole set
of declarations and input statements must be delimited by a
semicolon.
A complete description of the syntax and semantics of the input
format is given in the Appendix.
3
Preliminary User's Manual April 12, 1973
Example 3.
In an investigation of axiomatizations of elementary group theory the
following statements arose:
(1) x*x = y*y
(2) x*(y*y) = x
(3) x*(y*z) = z*(y*x)
(4) x*(x*y) = y
(5) (x*z)*(y*z) = x*y
Question: Does (5) follow from (1)-(4)?
The answer is "yes" but it is not immediately obvious. It is more
difficult to establish than Example 2. Notice that this example is a
pure equality formulation, (i.e., equality is the only predicate so
that all formulas are in fact equations). This example could be
presented to the prover as:
INF_OP: *;
INF_PRED: =;EQUALITY:=;
VAR: x,y,z;
AXIOMS: x*x = y*y;
x*(y*y) = x;
x*(y*z) = z*(y*x);
x*(x*y) = y;
THM:(x*z)*(y*z) = x*y;
;
In this example, the name AXIOMS, refers the first four statements.
Before presenting a more complicated example, we shall describe how
to use the prover on these first Examples.
4
Preliminary User's Manual April 12, 1973
Once the input file has been prepared you are ready to used the
theorem prover. The command: RUN PROVER [P,JRA] , will select the
current version of the program. The appearence of an asterisk (*)
signifies that the program is ready. If you wish the program to make
an initial selection of strategies for your problem then type:
(PROVE DSK: filename). The exact strategies which are chosen are
described in Section VIII. If you would rather select you own
strategies then type: (TRY DSK: filename). You will then be asked to
describe your choice and editing strategies. See Section VIII for a
complete description of strategy selection.
If the (translations of) the set of input statements are found to be
inconsistent, then the sequence of deductions which exhibits that
inconsistency is displayed on the console. This refutation and the
set of strategies which were employed are also saved on a disk file .
The name of the file is created from the name of the input file.
Thus, for example, (PROVE DSK: FOO) and (PROVE DSK: (FOO.A)) would
create an output file named N1FOO.PRF. If the input initially comes
for the console using (PROVE) or (TRY), then the output file is given
the name, N1PRF.PRF. It is also possible that the prover terminate
without finding a refutation. This could occur either because the
selected strategies do not form a complete set or because the initial
set is not inconsistent. In either case the program types NO-PROOF-
FOUND and enters the clause editor to wait for commands from the
user.
5
Preliminary User's Manual April 12, 1973
The first example is so simple that we shall just type it in on-
line. The output will then be found on the file N1PRF.PRF. Material
preceeded by | is commentary; statements typed by the user are
preceeded by *.
*RU PROVER [P,JRA] |retrieve the prover.
*(PROVE) |The prover is to pick strategies.
*PRE_PRED:A,B;
PRE_PRED:A,B; |Declaration is echoed by prover.
*HYPS: A⊃B;¬A⊃B;
HYPS |The statements are echoed.
A⊃B;
¬A⊃B;
*THM:B; |We wish to prove B.
THM
B;
*; |This final semicolon signals the end
|of the input.
HERE-ARE-THE-CLAUSES: |Here are the translations of the
|input statements.
1 A⊃B;
2 B∨A;
3 ¬B; |Notice that the statement of the
|theorem(THM) has been negated.
4 A; |The first deduction.
5 ¬A; |Another deduction.
COUNT 3
LEVEL 1 |These are statistics printed by the
ELAPSED-TIME 134 |prover.
6 B;
COUNT 5
LEVEL 2 |The end of level-2 deductions.
ELAPSED-TIME 288
|A proof has been found.
NIL 1 6 |Here's a proof-tree:
1 B; 3 4 | 6 5
3 A; 5 6 | \ /
4 A⊃B; HYPS | 3 4
5 B∨A; HYPS | \ /
6 ¬B; THM | 1 6
* | \ /
| NIL
Notes:
1. Though all statements are stored internally in conjunctive
normal form, an attempt is made to improve the readibility on
output. Clauses are translated for output as follows:
6
Preliminary User's Manual April 12, 1973
a)clauses containing only positive literals appear as a
disjunction.
b)clauses containing only negative leterals appear as the
negation of a conjunction.
c)mixed clauses, containing positive and negative literals
appear in the form of an implication.
7
Preliminary User's Manual April 12, 1973
Now let's try running the second example. Assume that a disk file,
EX1, has been prepared containing the axiomatization. What follows is
a running commentary on what should occur.
*RUN PROVER [P,JRA] |retrieve the current prover.
*(PROVE DSK: EX1) |Request that the program pick the
|strategies while running EX1.
PRE_PRED: P,G; |The program is accepting the axioms.
VAR: x,y,z;
G1:
∀(x,y)(P(x,y) ∧ P(y,z)) ⊃ G(x,z));
G2:
∀y∃x P(x,y);
THM:
∃(x,y)G(x,y);
HERE-ARE-THE-CLAUSES: |What follows are the translations
|of the input into clause-form, with
1 P(x,z)∧P(y,z) ⊃ G(x,y) |the redundant statements removed.
2 P(G21(x),x) |G21 is a generated Skolem function.
3 ¬G(x,y) |The translation of the negation of
|the theorem.
4 ¬(P(z,x)∧P(x,y)) |A deduction which has been added to
|the list of clauses.
COUNT = 1 |There was only one resolvent formed
LEVEL = 1 |on level one.
ELAPSED-TIME = 333 |The execution time in milliseconds.
5 ¬P(x,y);
COUNT = 3
LEVEL = 2 |Three resolvents have been formed by
ELAPSED-TIME = 500 |the end of level 2. (Two have been
|retained.)
NIL 1 4 |A contradiction. These next six
1 -P(x,y) 3 4 |lines are the refutation. I.e.:
3 ¬(P(z,x)∧P(x,y)) 5 6 | 6 5
4 P(G21(x),x) G2 | \ /
5 P(x,z)∧P(y,z) ⊃ G(x,y) G1 | 3 4
6 ¬G(x,y) THM | \ /
| 1 4
| \ /
| NIL
8
Preliminary User's Manual April 12, 1973
Notes:
1. The labeling of the input is reflected in the description
of the refutation tree. That is, P(G21(x),x) resulted from
the translation of G2; ¬G(x,y) came from the negation of the
theorem.
2. A copy of the refutation tree, relevant statistics, and a
description of the actual strategies used, now appears on a
file named N1EX1.PRF.
9
Preliminary User's Manual April 12, 1973
Now let's run the third example. Assume that the axiomatization is on
a file named EX2.
*RUN PROVER [P,JRA]
*(PROVE DSK: EX2) |Again, let the program
|pick the strategies.
INF_OP: *;
INF_PRED: =;
EQUALITY: =;
VAR:x,y,z;
AXIOMS:
x*x=y*y;
x*(y*y)=x;
x*(y*z)=z*(y*x);
x*(x*y)=y;
THM:
(x*z)*(y*z)=x*y;
HERE-ARE-THE-CLAUSES:
1 x*x=y*y
2 x*(y*y)=x
3 x*(y*z)=z*(y*x)
4 x*(x*y)=y
¬(THM1*THM3)*(THM2*THM3)=THM1*THM2
|Again, THMn's are generated
|Skolem constants.
NIL 1 2 |An immediate contradiction
1 x=x; |We know E is reflexive
2 ¬THM1*THM2=THM1*THM2; 3 4 |moderate mystery.
3 x*(y*z)=z*(y*x); AXIOMS
4 ¬(THM1*THM3)*(THM1*THM2)=THM1*THM2; THM
Notes:
1. The `refutation' is a bit mysterious. A more sympathetic proof
recovery mechanism is contemplated, but perhaps some of the current
mystery can be dispelled.
A `natural' proof might be:
1. (x*z)*(y*z) = z*(y*(x*z)) replacement using (3)
2. z*(y*(x*z)) = z*(z*(x*y)) replacement using (3)
3. z*(z*(x*y)) = x*y replacement using (4)
10
Preliminary User's Manual April 12, 1973
The above proof is indeed a translation of the machine proof.
Besides replacement, the prover also has a special rule of
simplification. Whenever an equality formulation is presented to the
prover, a list ,SL,is made consisting of all the equalities which
occur in the input. In the current example, SL would consist of
everything but the negation of the theorem. Let t1 = t2 be a member
of SL. Whenever a deduction is formed (but before it has been added
to the memory of the prover) we attempt to match t1 against terms
occurring in the deduction. If matches can be made we replace those
terms with the appropriate instance of t2. It is this simplified
deduction which is presented to the editing strategies of the prover.
11
Preliminary User's Manual April 12, 1973
Thus the refutation really is:
¬(THM1*THM3)*(THM2*THM3)=THM1*THM2 THEOREM
\
\
\ x*(y*z)=z*(y*x) AXIOMS
\ /
\ /
¬THM3*(THM2*(THM1*THM3))=THM1*THM2 by replacement
\
\
\ x*(y*z)=z*(y*x) AXIOMS
\ /
\ /
¬THM3*(THM3*(THM1*THM2))=THM1*THM2 by simplification
\
\
\ x*(x*y)=y AXIOMS
\ /
\ /
¬THM1*THM2=THM1*THM2 by simplification
\
\
\ x=x
\ /
\ /
NIL
by resolution
12
Preliminary User's Manual April 12, 1973
Most applications of the prover lie in that gray area between a quick
proof and the occurrence of NO-PROOF. That is, an application of the
prover usually generates a large number of deductions before either a
proof is found or no more deductions can be made under the current
strategy settings. It is this area which can be profitably explored
using interactive commands. If the user sees a deduction which
should lead to the desired refutation he is able to guide the
program to the explicit contradiction. If he sees a deduction which
he feels is interesting, he can explore its consequences in the set
of statements. If he feels that the strategy settings are ill-chosen
then he can abort the current proof-search and pick new strategies.
The next sections give detailed descriptions of the current on-line
commands.
First, the on-line editor is entered by striking the space bar.
I. GENERAL BOOKEEPING COMMANDS.
CHange CH;
It is frequently desireable to change some of the
strategies while a proof attempt is in progress.
CHange describes what choice and editing strategies
are currently active and asks which are to be
changed.
CUrrent CU;
This command simply lists the current strategy
settings.
DSkout DS <filename>;
This command diverts future output to specified disk
file.
13
Preliminary User's Manual April 12, 1973
EVal EV;
This command is mostly a debugging aid and is
included for completeness. The casual users should
not have to resort to its use. EVal enters a READ-
EVAL-PRINT. To return to the editor, type @END.
HAlt HA;
HAlt stops the prover is such a state that if the
current core image is saved, it can be continued. To
resume execution of such a core image, type RUN DSK:
name. When the asterisk appears you are in the on-
line editor. Then type TErminate.
End Of file EO;
EOf is used to terminate the DSkout command.
HElp HE;
This command will type a list of the available
editing commands along with an abbreviated
description of their action.
TErminate TE;
This command is used to terminate the use of the on-
line editor and return to the prover.
14
Preliminary User's Manual April 12, 1973
II. COMMANDS TO EXAMINE THE LIST OF CLAUSES
Each clause which has been retained by the prover -- initial clauses
or deduction -- is given a number, the first axiom, the number 1.,
etc.. These numbers are permanently assigned, even though certain
actions of the prover may delete clauses from active status in which
case they are not used in making any future deductions. Clauses
which have been so deleted are displayed as *DE*. When the editor is
entered, a hypothetical pointer is initialized to the first clause.
This first set of commands allow the used to manipulate the set of
clauses using the associated numbers.
FLoat UP FU; or FL UP;
Moves the pointer up through the list of clauses.
The motion is stopped either by striking a key or by
reaching the upper extreme of the list. FLoat UP may
also be apbbreviated as FU.
FLoat DOwn FD; or FL DO;
The counterpart of FLoat UP. FLoat Down may also be
abbreviated as FD.
UP UP n;
UP is to be followed by an integer, n. The effect of
this command is to move the pointer up n clauses from
its current setting. As the pointer is moved, the
interviening clauses are printed. If n = 0, then the
pointer is immediately moved to the beginning of the
clause list. As with the FLoat commands,striking a
key will stop the pointer.
DOwn DO n;
The counterpart of UP. DOwn 0 moves the pointer to
the end of the list.
GO GO n;
15
Preliminary User's Manual April 12, 1973
GO is to be followed by an integer designating a
clauses. The pointer goes immediately to the
designated clause.
16
Preliminary User's Manual April 12, 1973
Though these commands have proved quite useful, experience has
shown that more global manipulation of the clauses is needed.
Therefore we have commands for assigning names to subsets of the
clause list, and commands for manipulating these sets. Just as each
element of the primary list of clauses is assigned a unique positive
integer, so is each element of each named subset. For example to
refer to the second element of the set named FOO, use FOO[2]; to
refer to the second and third elements, use FOO[2,3]. Certain
commands, like REsolve or PAramodualte create new names, like
RES1,RES2, etc. or PAR1, PAR2. These created names are local to that
call on the on-line editor. Names which were initiated by the user
using the SEt command are global.
The following BNF equations will be used in the sequel:
<clauses> ::= {<c>,}*<c>
<c> ::= <number>|<id>{[{<number>,}*<number>]}*
::= @<statment>|FIND[<id>;<pattern>]
ANcestry AN <clauses>;
The ancestry command is used to display the
derivation tree of the specified clauses.
CLear CL <id>;
CLear takes a name as argument. This command only
removes the name from the symbol table; it does not
affect the clauses attached to the name.
Delete DE <clauses>;
The designated clauses are deleted from the memory of
the prover. Attempts to display such clauses will
17
Preliminary User's Manual April 12, 1973
print *DE*. Other attempts to use deleted clauses in
editing commands will invoke an error message.
DIsplay DI <clauses>;
This command displays all the elements of <clauses>;_
INsert IN <id> <statements>; IN <id> DSK: <file>;
This command is used to enter new clauses into the
clause editor. The first argument to INsert is a
<name>. What follows is a set of clauses, or a file
designator. If the clauses are typed they must
conform to the standard input format; if a file
designator is given, the specified file must be in
the correct format. IN is a special case of the SEt
command.
SAve SA <clauses>;
Most of the results of the on-line commands:
deductions, insertions, substitutions,etc, are local
to the clause editor. To include any of these
resulting clauses in the memory of the prover use the
Save command.
SEt SE <id> <clauses>;
SEt <id> <clauses>; has the effect of assigning to
<id>, the sequence of clauses selected by the
<clauses>. Within a particular proof attempt, the
names selected by the user are retained.
SUbstitute SU <term>; FOR <term>; IN <clauses>;
The effect of the SUbstitute command is to substitute
the first <term> for every occurrence of the second
<term> in copies of all of the designated <clauses>.
Notice that the original <clauses> are kept intact.
The modified <clauses> are added to the list named
ASSERT.
18
Preliminary User's Manual April 12, 1973
The commands listed above give us a reasonably powerful set of
instructions for manipulating the clause list. Clearly, before we can
really begin to guide the prover we must be able to perform the rules
of inference on-line. The next set of commands begins to do this.
III. COMMANDS FOR PERFORMING RULES OF INFERENCE
PAramodulate PA <clauses>; <clauses>;
This command handles equality replacements. All
equality literals of the form t1=t2, are used in
equality replacements in the following manner: let s
be any term, not a variable, which occurs in some
literal in one of the clauses. If s occurs no deeper
than PDEPTH (see the appendix for PDEPTH) and there
is a substitution unifying s and t1, then the
occurrence of t1 is replaced by the appropriate
instantiation of t2.
REsolve RE <clauses>;<clauses>;
This command takes a pair of <clauses> as arguments.
The resolvents of these two sets are formed, a unique
name is generated and the resolvents are assigned to
that new name. The generated names are presently of
the form RESn, for some integer,n.
SImplify SImplify <clauses>; BY <clauses>;
This command is similar to the PA command. Here the
second set of clauses is to be a list of equality
units, again of the form t1=t2. Terms occuring in the
first set of clauses which unify with elements, t1,
are replaced by instances of t2. DDEPTH determines
the depth to which the match is attempted.
Example 3. A simple example of the use of the rules of inference.
Assume that = is the equality predicate and that we have just struck
a key on the console.
*DI 1,2,3; |Display the first three clauses
1 x≤y ⊃ x/y=0
2 ¬1/(a/b)=0
19
Preliminary User's Manual April 12, 1973
3 0≤x
*PA 1; 2; |Use replacement on 1 and 2.
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME: PAR1 |PAR1 is a created name.
1 1≤a/b ⊃ 1=0
*PA 2; 3; |Try to use the replacement rule
NO-PARAMODULANTS |on clauses 2, and 3.
*RE 1; 3;
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME:RES1 |RES1 is another created
|name.
1 0/x=0
*PA RES1; RES1; |Created names are legal.
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME:PAR2 |PAR2 is a new name.
1 0=0 |True.
*SA PAR1[1]; |Add 1≤a/b ⊃ 1=0 to the memory
|of the prover;
20
Preliminary User's Manual April 12, 1973
IV. COMMANDS FOR SUB-PROOFS AND PROOF-CHECKING.
Though the commands, REsolve and PAramodulate, are useful for fine
control of the prover, is is often useful to demand larger inference
steps. That is, using some of the existing clauses in memory, with
perhaps some additional assumptions, we wish the prover to attempt to
establish the validity of a first order formula. While this subproof
is under investigation the state of the main proof should be
preserved. The commands in this section are used to initiate and
control such subproofs.
ABort AB ; or AB <clauses>;
This command is used to manually abort a proof
attempt, returning to the previous level. If
<clauses> is present, then the selected clauses are
returned and assigned to a created name.
USing US <clauses>; or US DSK: <file>;
The selected clauses are designated to be used in the
forthcoming subproof.
PRove PR <statement>; or PR DSK: <file>;
The <statement> is translated and will be attached to
the name LEMMA. The negation of the statement is also
formed and will be used in the subproof. Thus both
the positive and negative tanslates are formed. The
positive translate is maintained for the convenience
of the user since after the lemma has been
established it should be available for further
deductions. Within the subproof the negation of the
<statement> will appear under the local name, THMS.
These last two commands,--USing, and PRove -- are used to initialize
the call on the prover; USing may be omitted. There are two commands
to commence the subproof.
EXecute EX;
21
Preliminary User's Manual April 12, 1973
EXecute begins the subproof using a computed set of
stategies.
TRy TR;
TRy first enters the strategy selection dialog, then
begins the subproof with the chosen strategies.
In both cases the strategies of the subproof are completely local.
They in no way affect the strategies in the parent proof. If a key is
struck while in the subproof the editor is entered and can manipulate
the local clauselist or initiate another subproof. The TErminate
command will comtinue the subproof, the ABort command will return to
the previous level.
22
Preliminary User's Manual April 12, 1973
Example 3. A simple example of subproof generation.
Suppose that we have struck a key during a proof-search.
*AN 10; |Display the ancestry of
P(A) 1 2 |clause no. 10.
1 P(A) ∨ P(B) AX1
2 ¬P(B) HYP1
*USING 10, @P(A) ⊃ P(B); ; |Setup the assumptions for the
|lemma.
|Use clause no. 10 in the attempt
*PROVE @P(B);;
*EX; |This initiates the subproof.
NIL 1 2
1 P(A) DEDUCT |Clause 10 becomes an "axiom"
2 ¬P(A) 3 4 |with the subproof.
3 P(A)⊃P(B) INSERT
4 ¬P(B) THM |The negation of the lemma
PROOF-FOUND-FOR-LEMMA
|We are now back in the editor
*DI 10; |Display clause no. 10.
P(A)
*DI LEMMA; |The translate of the statement
P(B) |to be PROVEed.
*USING LEMMA;
*PROVE @∃(x)P(x);; |LEMMA now becomes the translate
*EX; |this clause.
NIL 1 2
1 P(B) AX1
2 ¬P(X1) THM
PROOF-FOUND-FOR-LEMMA
*DI LEMMA; |ED1 is a ubiquitous Skolem
P(ED1) |constant.
23
Preliminary User's Manual April 12, 1973
V. COMMANDS USEFUL WHEN NO PROOF IS FOUND
When the prover is unable to make new deductions which satisfy the
current strategies it will report that no refutation can be found,
and will enter the on-line editor. At this time the user can examine
the list of clauses, perform rules of inference, initiate sub-proofs,
save any or all of the current deductions and begin a the proof
search again, perhaps with new strategies. The user can also force a
proof attempt to be abandoned by typing AB;. This has exactly the
same effect as if the prover could make no new deductions.
ABandon AB;
AB, typed in this context (not in a subproof)
terminates the main proof attempt, enters the on-line
editor, and waits for commands.
TErminate TE <clauses>; or TE;
If <clauses> are present then they are added to the
list of clauses named THMS. The list, AXIOMS, HYPS,
and THMS are preserved and a new proof attempt is
begun. If the initial attempt was through PROVE then
the user is asked if he still wants automatic
strategy selection. If the initial attempt was
through TRY or the user does not wish automatic
selection, then a dialogue is begun describing the
current strategies and asking if changes are desired.
Then a new proof search is begun.
This use of AB and TE is useful for feeding `interesting' deductions
back into a proof search without having to restart the whole process.
The derivation tree of any such saved derived clause is maintained
for the proof recovery mechanisms but such clauses appear to be
`input' clauses to the rules of inference.
24
Preliminary User's Manual April 12, 1973
V. SEARCHING AND PATTERN MATCHING.
This section is a preliminary account of certain features of the
current system which are being extended and developed further.
The pattern matching facilities for interactive theorem proving are
the most difficult feature to describe well. The tools presented to
the user should be general enough to significantly aid in the search
for a proof. At the same time the pattern matching commands should
be concise and somewhat readable. Clearly, pattern matching is
present throughout the theorem prover; the choice strategies, the
rules of inference, and the editing strategies are all examples of
very sophisticated pattern matching. Thus pattern matching is very
important part of the theorem proving process. Currently, a very
simple pattern matching facility is available.
Pattern matching is invoked by the FIND operation.
FIND[<id>,<pattern>] expects <id> to be the name of a list of
clauses, and <pattern> should be a Boolean combination of primitive
patterns. These primitive patterns are described in the next section,
but basically allow description of syntactic parts of clauses.
Since many of the applications of FIND are of the form
FIND[CLAUSES,<pattern>], the abbreviation, FINDC[<pattern>] has been
added for this case.
Here's an example of FIND and FINDC.
SET XX FINDC[OCR[0]]; |OCR is a reserved word. The pattern says
|find all clauses in the set CLAUSES which
|have occurrences of the symbol 0.
|In this problem 0 is a function letter.
*
25
Preliminary User's Manual April 12, 1973
DI XX; |Display the clauses.
1 x/y=0 ⊃ x≤y;
2 x≤y ⊃ x/y=0;
3 0≤x;
4 x/x=0;
5 x/1=0;
*
SET YY FIND[XX,OCR[≤]]; |Find clauses in XX which have occurrences
|of the symbol '≤', and assign those clauses
|to YY.
*
DI YY; |Display YY.
1 x/y=0 ⊃ x≤y;
2 x≤y ⊃ x/y=0;
*
*
SET ZZ FIND[YY,OCR[/]∧OCR[=]];|Boolean combinations are allowed.
*
SET ZZ FIND[YY,LENGTH=1];|This command will locate all units in the
|set, YY.
26
Preliminary User's Manual April 12, 1973
VI. PRIMITIVE PATTERN LANGUAGE.
The currently available primitives allow description of ancestry of
a clause, the length(number of literals) and depth(of function
nesting) of clauses,besides a very simple matching algorithm. The
matcher looks for matches on literals ,terms, predicate letters,
negations of predicate letters, or fuctions symbols.
PRIMITIVES:
1) primitive for ancestry: TREE[x]
"x" designates a clause. TREE[x] will match any clause whose
derivation tree contains x. N.B. the clause ,x, itself is
considered to be derived from x.
Examples:
For example, if G1 is the name of an initial statement then :
SET YY FIND[XX,TREE[G1]]; will assign to YY all of the clauses in XX
which were derived using G1.
2) primitive for length: LENGTH
LENGTH gives the number of literals in the clauses currenly being
examined. LENGTH may be tested using one of the available operators.
Examples:
LENGTH = 1 is true of the current clauses is a unit.
3) primitive for depth: DEPTH
This primitive gives the depth of function nesting in the clause.
Example:
27
Preliminary User's Manual April 12, 1973
DEPTH > 4 is true is the depth of nesting of the current clause is
greater than 4.
Primitive relations:
Currently the only relations available are =,>,and <. These
relations are only to be used in comparing length and depth.
MATCHING:
4) primitive for matching: OCR
OCR is the implementation of a simple matcher which expects its
arguments to be a literal, term, predicate letter, or negation of a
predicate letter. OCR matches any clause which contains a matching
construct.
Variables may appear in the pattern, in which case a test for
subsumption determines when a match is to be successful.
Examples:
In the following, assume P, and = are predicate letters; assume x,y,
and z are variables; and assume a,b,c,d and f and g are function
symbols.
OCR[P] matches P(x) ,P(a)⊃a=b, and ¬P(b).
OCR[¬P] matches P(a)⊃a=b and ¬P(b). Note P(a)⊃a=b matches here since
the implication really is ¬P(a) ∨ a=b;
OCR[¬=]∧¬OCR[d] would match ¬f(a,b)=c but would not match ¬f(a,b)=d.
OCR[P(x)] matches P(x),¬P(g(x)) and ¬P(a).
OCR[¬P(g(x))] matches ¬P(g(a)) but not P(g(a)) or ¬P(f(g(a),x));
28
Preliminary User's Manual April 12, 1973
OCR[f(g(x),x)] matches clauses containing say, f(g(a),a) but does not
match f(g(a)b).
29
Preliminary User's Manual April 12, 1973
VII. GETTING ALONG WITH THE SYSTEM.
1) Running the prover.
RU PROVER [P,JRA]
(PROVE | TRY <input>) ;<input> is either a DSKfile or null.
2) Saving a core image.
Hit space bar.
The prover responds by typing its first clause.
Now type HAlt.
Response: "HALT AT USER ####".
You may now save the core image.
Typing "ST" or "RUN"-ing the saved image will
have the same effect: the prover will respond
"*" and you will be back in the on-line editor.
You may continue the proof search by typing
"TErminate".
3) Reallocation.
Frequently it is desireable to increase the storage areas during the
execution of the prover without having to restart the whole problem.
This can be done as follows:
Hit the space bar.
Call the monitor.
Execute "ST 141".
Call the monitor.
Execute "CORE #".
Execute "ST".
Evaluate "(REENTER)".
The prover will now resume its computation
in the enlarged work spaces.
30
Preliminary User's Manual April 12, 1973
31
Preliminary User's Manual April 12, 1973
Frequently the user of a theorem prover "knows" a lot of detail about
the problem domain being axiomatized. Much of this information
(almost by definiton) is domain-dependent and thus doesn't fit the
usual set of strategies as well as could be desired. Also much of
this information is heuristic in nature and would be difficlut to
express in the form of axioms. To help with these problems we have
introduced two new ideas: (1) a language for describing strategies;
and (2) new data types have been added to LISP so that the user may
tailor-make his own prover.
The strategy language allows Boolean expressions over properties of
clauses. Major extensions of this idea are contemplated..
The programmable aspects allow the user to describe first order
statements, strategies and pattern matching in an intuitive notation.
With these facilities inside LISP we can write new rules of inference
and domain dependent theorem provers.
33
Preliminary User's Manual April 12, 1973
VIII. The Language of Strategies.
(1) Choice strategies.
Choice strategies occur in the following context: Given two possible
candidates,C1 and C2, for the application of a binary rule of
inference, I, a choice strategy will determine whether not we wish to
form I(C1,C2).
Builtin choice strategies.
a) NONE allows unrestricted applications of the rules of inference.
b) ANCESTRY implements the AFF strategy; that is, to apply I either
C1 or C2 must be an initial clauses, or, either C1 appears in the
derivation tree of C2, or C2 appears in the tree of C1.
c) SUPPORT designates the set-of-support strategy. This strategy
basically says that every first-level deduction must have one of its
parents in the support set. SUPPORT must be followed by an argument
list describing which statements are to be supported. The elements
of the argument list may either be clause numbers or names which the
user has associated with certain input clauses.
Example: SUPPORT[1,2,AXIOM[2],THEOREM] would put clauses numbered 1
and 2, the clause AXIOM[2], and all clauses with name, THEOREM, in
the support set.
d) VINE strategy says that either C1 or C2 must be an initial clause.
This strategy is known to be incomplete, but is useful in many cases.
e) UNIT strategy says that either C1 or C2 are singletons. Again,
34
Preliminary User's Manual April 12, 1973
this strategy is not complete ,but is useful as a "quick-kill" or
"end-game" strategy. It is easy to show that if there is a UNIT-
refutation then there is a VINE-form refutation. It is also easy to
show that if all the initial statements are either units(singletons)
or are of the form L1∧L2∧...∧Ln ⊃ M then there is a UNIT proof.
f) P1 is the P1-deduction of Robinson. Here it is required that
either C1 or C2 contain only positive literals. This strategy is
complete.
g) MODEL is the implementation of a very simple case of the model-
relative deduction strategy of Luckham. Model-relative deduction is
a generalization of P1 deduction and is complete. Deduction relative
to a model says that at least one of the clauses C1 or C2 be false of
the model. MODEL expects an argument list describing a binary
partition of the predicate letters appearing in the initial clauses.
In the current restricted implementation this says either C1 or C2
must have zero intersection with the two members of the partition.
h) DEFMODEL can be used to designate a LISP function to define a
model for the current set of statements. DEFMODEL expects a single
argument which is the name of a LISP function(of one argument) and
which implements the defining conditions of a model.
i) EQUALITY signals that the replacement rule, paramodulation, is to
be used. EQUALITY needs two arguments: a predicate name to be
interpreted as equality; and second, a number, called PDEPTH, which
35
Preliminary User's Manual April 12, 1973
determines how deep in the nesting of function symbols the matcher
will look in attempting to match terms. For example, a PDEPTH of 1
says only examine primary occurences of terms.
36
Preliminary User's Manual April 12, 1973
(2) Editing Strategies.
Editing strategies are applied to the results of the rules of
inference. These strategies are used to filter out some of the
deductions which a rule of inference has generated.
Builtin editing strategies.
a) DEMOD is a rule of simplification most commonly used in
conjunction with EQUALITY. DEMOD takes two arguments. The first
describes a list of equality units; the second, a number named DDEPTH
which,like PDEPTH, determines a bound on the matching routines.
b) DEPTH takes a single integer argument interpreted to be a bound on
the depth of function symbol nesting which must not be exceeded if
the deduction is to be retained.
For example, DEPTH[4].
c) LENGTH also takes an integer argument and gives a bound on the
number of literals which will be allowed in any deduction.
d) SELDEPTH takes function symbol-number pairs as arguments.
SELDEPTH is a refinement of DEPTH in that the allowable depth of
nesting of each function symbol is determined by the corresponding
number.
e) Any of the primitive constructs of the pattern language: TREE,
LENGTH, DEPTH, or OCR. For example if OCR[f(e,e)] were to appear in
an editing strategy then any clauses which contained "f(e,e)" would
be rejected.
37
Preliminary User's Manual April 12, 1973
Boolean combinations of built-in or user-defined strategies are
allowed. For example, a reasonable choice strategy is: ancestry
filter form with a set of support being the negation of the statement
to be proved. This can be written as:
ANCESTRY ∧ SUPPORT[THEOREM];
An editing strategy which filters out all clauses whose length(number
of literals) is greater than 4 or whose depth( depth of nesting of
function symbols) is greater than 3 can be expressed as:
LENGTH[4] ∨ DEPTH [3];
3) The Automatic Strategy Selection.
A very simple procedure is used to select the strategies in PROVE-
mode. The choice strategies are ANCESTRY and, if THEOREMNAME is
present as an axiom name ,then SUPPORT[<value of THEOREMNAME>] is
also used. Also, if an equality predicate letter is declared, then
equality replacement witha depth bound of 4 is added.
The editing strategies are determined by the maximum lengths and
depths which occur in the input clauses. If equality is present then
a simplification list consisting of all the positive units is used.
The strategy settings are automatically changed if the program is
terminated without finding a proof.
38
Preliminary User's Manual April 12, 1973
IX. Theorem proving primitives.
It is now possible to write LISP-like programs which control the
actions of the theorem prover and manipulate clauses. Data types
for CLAUSES, STRATEGIES, and PATTERNS have been added to LISP so that
the user can describe his clause manipulations in the same notation
which is used to drive the on-line prover. LISP functions, TRYTIL
and FIND, have been defined to perform controlled proof-attempts and
clause-list searching.
1. Data Types.
a) [CLAUSES <clauses>] is used to introduce new clause lists to the
program. For example: (SETQ X [CLAUSES DSK:FOO]) when executed will
assign to X the clauselist manufactured from the statements on file
FOO.
b) [CHOICE <strategy>] and [EDIT <strategy>] introduce the
appropriate strategies.
c) [PATTERN <pattern>] is useful in conjunction with FIND to filter
out clauses which match <pattern>.
2. Procedures.
(TRYTIL <clauses><choice-strategy><edit-strategy><termination
condition>)
where: 1) <clauses> is a list of clauses . 2) <choice-strategy> is a
representation of a choice strategy. 3) <edit-strategy> represents
an editing strategy. 4) <termination condition> is a functional
39
Preliminary User's Manual April 12, 1973
argument which will be evaluated periodically during the execution of
the TRYTIL. As long as the condition evaluated to NIL the proof
attempt will continue. If the condition becomes true then TRYTIL will
return the list of all deductions which have been made.
For example:
(TRYTIL [CLAUSES DSK: FOO] [CHOICE ANCESTRY∧SUPPORT[THEOREM]] [EDIT
LENGTH[4]∨DEPTH[3]] (FUNCTION (LAMBDA()(GREATERP LEVEL 3))) )
will begin a proof search using file DSK:FOO with choice strategy
being AFF and supporting the negation of the theorem. Deductions
whose length is greater than 4 or whose depth of fuction nesting is
greater than 3 will be discarded. The proof search will terminate at
the end of level 3.
If a refutation is discovered during any attempt, (QED) is returned.
If no refutation is found, then the on-line editor is called to give
the user a chance to examine the current proof environment. There is
a third way to exit TRYTIL: since the on-line editor is available
inside the proof attempt, typing ABandon <clauses> to the editor
will force termination of the proof attempt and will return the
selected <clauses>.
(FIND <clauses><pattern>)
where: 1) <clauses> is a list of clauses. 2) <pattern> is a
condition which is to be applied to each element of <clauses>.
The value of FIND is a list of all elements of <clauses> which
satisfy the <pattern>.
40
Preliminary User's Manual April 12, 1973
X. THE ANSWER EXTRACTOR
A subset of the Luckham-Nilsson answer-extraction algorithm has been
implemented. It is not available as part of the basic prover, but
must be loaded by the user. The prover should run in slightly more
core to accommodate the answer routines.
Here is an example:
Recall example 2. in the introduction:
(1) ∀(x,y)P(x,y)∧P(y,z)⊃G(x,z)
(2) ∀y∃xP(x,y)
Question:(3) ∃(x,y)G(x,y) .
From the semantics of the problem we know that the "answer" to (3) is
"yes" and in fact we can display specific solutions to the problem:
The parent of the parent is the grandparent. What does the answer
extractor do with this problem?
RU DSK PROVER[P,JRA] ;get the prover
(DSKIN (P,JRA) ANSWER) ;load in answer extractor
(PROVE DSK: EX1)
...
[output as before]
...
*(ANSPRED) ;this calls the extr!ctor
*G(G21(G21(x)),x) ;the answer
*
We must now interpret the Skolem function, G21. G21 was introduced
in the translation of (2), that is, G21(y) is an object such that
P(G21(y),y). Thus G21 is a function to select the parent of an
individual. In this light our answer, G(G21(G21(x)),x), is the
expected result.
The current implementation of the answer extractor does not
41
Preliminary User's Manual April 12, 1973
recognize applications of the equality rule and will fail to get
answers in this case. It is trivial to extend the algorithm and its
implementation will occur shortly.
42
Preliminary User's Manual April 12, 1973
APPENDIX
THE SYNTAX EQUATIONS FOR THE THEOREM PROVER.
The parsers for the input syntax and the command language are both
contstructed by Lynn Quam's Syntax Directed Input Output program.
THE SIMPLE STRATEGY LANGUAGE
The most straightforwrd application of the strategy language consists
of using Boolean combinations of the builtin strategies.
<STRATEGY>::=<F1>;
<F1> ::=<F2>
::=<F1><OR><F2>
<F2> ::=<F3>
::=<F2><AND><F3>
<F3> ::=(<F1>)
::=<NOT><F3>
::=<PREDIC>
<PREDIC>::=ANCESTRY
::=NONE
::=VINE
::=UNIT
::=P1
::=SUPPORT[<C>]
::=MODEL[<PREDLST>;<PREDLST>]
::=EQUALITY[<OP>,<NUMBER>]
::=DEMOD[<CLAUSES>,<NUMBER>]
::=DEFMODEL[ID]
::=LENGTH[<NUMBER>]
::=DEPTH[<NUMBER>]
::=SELDEPTH[<FNLST>]
::=<MPRM>
<PREDLST>
::=<ID>,<PREDLST>
::=<ID>
::=
<FNLST> ::= <FP>;<FNLST>
::= <FP>
43
Preliminary User's Manual April 12, 1973
<FP> ::=<OP>,<NUMBER>
44
Preliminary User's Manual April 12, 1973
THE INPUT FORMAT
The usual form for input consists of the declarations of the non-
logical constituents of the axioms, followed by a sequence of
statements. The statements may be assigned names, and if a statement
whose name is the same as the current value of THEOREMNAME is present
that statement is negated before being added to the memory of the
prover.
<INPUT> ::=<DECOP>:<OPLIST>;
::=<ID>:
::=<S>
<DECOP> ::=VAR | INF_OP | INF_PRED | PRE_OP | PRE_PRED | EQUALITY
<OPLIST>::=<OP>,<OPLIST>
::=<OP>
<S> ::=;
::=<S1>;
<S1> ::=<S2>
::=<S1><EQUIV><S2>
<S2> ::=<S3>
::=<S2><IMP><S3>
<S3> ::=<S4>
::=<S3><OR><S4>
<S4> ::=<S5>
::=<S4><AND><S5>
<S5> ::=(<S1>)
::=<NOT><S5>
::=<QFF><BODY>
::=<PRED>
<BODY> ::= <IVAR><S5>
::=(<VARLIST>)<S5>
<VARLIST>::=<IVAR>,<VARLIST>
::=<IVAR>
45
Preliminary User's Manual April 12, 1973
In the following,the routines corresponding to <PREPREDLET>,
<INFPREDLET>, <IVAR>, <PREFN>, and <INFN> check the lists of prefix-
and infix- predicate and function letters, and the variable list, all
of which were manufactured by the appropriate declarations.
<PRED> ::=<PREPREDLET><ITMLST>
::=<TM><INFPREDLET><TM>
<ITMLST>::=(<ITMS>)
<ITMS> ::=<TM><ITMS>
::=<TM>
<TM> ::=<IVAR>
::=<PREFN><ITMLST>
::=<PREFN>
::=(<TM>)
::=<TM><INFN><TM>
The logical connectives are defined as follows:
<EQUIV> ::= ≡ | ↔
<IMP> ::= ⊃
<OR> ::= ∨
<AND> ::= ∧
<NOT> ::= ¬
<QFF> ::= ∀ | ∃
46
Preliminary User's Manual April 12, 1973
THE COMMAND LANGUAGE
<CLAUSES> ::= <C>,<CLAUSES>
::= <C>
<C> ::= @<S>
::= DSK: <FILE>
::= <NUMBER>
::= <ID>[<VARLIST>]
::= <ID>
::= FIND [<ID>,<MATCH>]
::= FINDC [<MATCH>]
<FILE> ::= <ID>
::= (<ID>.<ID>)
<VARLIST> ::= <NUMBER>,<VARLIST>
::= <NUMBER>
<COMMAND ::= AB <CLAUSES>;
::= AB;
::= AN <CLAUSES>;
::= CH;
::= CL <ID>;
::= CU;
::= DE <CLAUSES>;
::= DI <CLAUSES>;
::= DO <NUMBER>;
::= DS <FILE>;
::= EO;
::= EV;
::= EX;
::= FD;
::= FU;
::= GO <NUMBER>;
::= HA;
::= HE;
::= IN <ID> <CLAUSES>;
::= ME <CLAUSES>;<CLAUSES>;
47
Preliminary User's Manual April 12, 1973
::= PA <CLAUSES>;CLAUSES>;
::= PR <CLAUSES>;
::= RE <CLAUSES>;<CLAUSES>;
::= SA <CLAUSES>;
::= SE <ID> <CLAUSES>;
::= SI <CLAUSES>; BY <CLAUSES>;
::= SU <TM> FOR <TM> IN <CLAUSES>;
::= SY;
::= TE <CLAUSES>;
::= TE;
::= UP <NUMBER>;
48
Preliminary User's Manual April 12, 1973
THE MATCHER
<MATCH> ::= <M2>
::=<MATCH> ∨ <M2>
<M2> ::= <M3>
::= <M2> ∧ <M3>
<M3> ::= (<F1>)
::=¬<M3>
::=<MPRM>
<MPRM> ::= <ARG><MOP><ARG1>
::= OCR[<PAT>]
::=TREE[<CNAME>]
<MOP> ::= =
::= <
::= >
<ARG1> ::= <ARG>
<ARG> ::= LENGTH
::=DEPTH
::=<NUMBER>
<CNAME> ::= <NUMBER>
::= <ID>[<VARLIST>]
::= <ID>
<PAT> ::= <NOT1><PRED>
::=<PRED>
::=<TM>
::=<FNLET>
49